package sketch.issta11.specifyoracles;

import java.util.LinkedList;
import java.util.List;

import junit.framework.TestCase;

import sketch.ounit.Observer;
import sketch.specs.annotation.Repl;
import sketch.specs.annotation.TestSketch;

public class Z_ObserverOracles_Example extends TestCase {

	@TestSketch
	public void testObserveLength() {
		List<String> l = new LinkedList<String>();
		l.add("1");
		l.add("2");
		{/*@ChooseOne*/
			l.add("3");
			l.remove(0);
		}
		Observer.observeExpr(l.size());
		Observer.observeExpr(l.toString());
		if(l.size() > 2) {
			Observer.observeExpr(l.getClass().toString());
		}
	}
	
	@TestSketch
	@Repl(source={"clear"}, dest={"toString"})
	public void testObserveLength_withReplace() {
		List<String> l = new LinkedList<String>();
		l.add("1");
		l.clear();
		Observer.observeExpr(l.isEmpty());
	}
	
	@TestSketch
	public void testNullOrNotNull() {
		List<String> l = null;
		{/*@ChooseAllOrNone*/
			l = new LinkedList<String>();
		}
		Observer.observeExpr(l);
	}
	
	@TestSketch
	public void testObserveEquality() {
		List<String> l1 = new LinkedList<String>();
		l1.add("1");
		List<String> l2 = new LinkedList<String>();
		{/*@ChooseOne*/
			l2.add("1");
			l2.add("2");
		}
		Observer.observeEquality(l1, l2);
	}
}
